a, b:. ((a  b) ~ tt)  {(a ~ tt) & (b ~ tt)} 

latex

ProofTree

Definitions	SQType(T), {T}, left + right, Unit, P  Q, x:A  B(x), x:AB(x), , , s = t, b, A, b, x:A. B(x), t  T, P  Q, s ~ t, P & Q
Lemmas	assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool sq